# -*- coding: utf-8 -*-

import random
import copy
import re

from alphabet import Alphabet
from error import LTSError
from state import State
import utils

_TOP_OF_THE_STACK = -1

class LTS:
	"""
		Esta clase representa un Labelled Transition System.
		
		Las instancias de esta clase sirven para reprecentar tres tipos de 
		sistemas: lts, diagnoser y twin-plant.
	"""
	
	### Atributos.
	
	# Nombre del LTS.
	name = ''
	# Referencia al estado inicial.
	init_state = None
	# Dice si es diagnosticable o no.
	isdiag = None
	
	def __init__ (self, init_state=None):
		self._alphabet = Alphabet()
		self._states = set()
		self._twinplant = None
		self._recalc_tp = True
		self.init_state = init_state
		self.name = 'LTS-'+str(int(random.random()*100))
	
	### Metodos para el alfabeto.
	
	def set_alphabet(self, alphabet):
		"""
			Descripcion:
				Establece el alfabaeto del sistema.
			Argumentos:
				alphabet	-	Una instalcia de la clase Alphabet().
			Retorno:
				No tiene.
		"""
		self._alphabet = alphabet
	
	def get_alphabet(self):
		"""
			Descripcion:
				Devuelve el alfabaeto del sistema.
				NOTA: Devuelve una referencia al alfabeto, no una copia de el.
			Argumentos:
				No tiene.
			Retorno:
				Una instalcia de la clase Alphabet().
		"""
		return self._alphabet
	
	### Metodos para los estados.
	
	def add_state(self, s):
		"""
			Descripcion:
				Agrega un estado al sistema.
			Argumentos:
				s	-	Instancia de la clase State() a agregar.
			Retorno:
				No tiene.
		"""
		self._states.add(s)
		if s.init:
			self.init_state = s
		self._recalc_tp = True
	
	def remove_state (self, s):
		"""
			Descripcion:
				Remueve un estado del sistema.
			Argumentos:
				s	-	Instancia de la clase State() a eliminar.
			Retorno:
				No tiene.
		"""
		self._states.remove(s)
		if s.init:
			self.init_state = None
		self._recalc_tp = True
	
	def is_state (self, s):
		"""
			Descripcion:
				Dice si un estado esta precente en el sistema o no.
			Argumentos:
				s	-	Instancia de la clase State().
			Retorno:
				True	-	Si 's' es un estado del sistema.
				False	-	Caso contrario.
		"""
		return s in self._states
	
	def get_states_by_name (self, state_name):
		"""
			Descripcion:
				Devuelve una lista de estados con el mismo nombre.
			Argumentos:
				state_name	-	Cadena de caracteres que reprecenta un nombre 
								de estado.
			Retorno:
				Una instancia de la clase List() cuyos elementos son instancias 
				de la clase State() los cuales tienen por nombre a "state_name".
		"""
		return [s for s in self._states if s.name == state_name]
	
	def get_state (self, state):
		"""
			Descripcion:
				Devuelve una referencia a un estado 's' del sistema que cumpla 
				's == state'.
				NOTA: Dos estados son iguales cuando los atributos 'name', 
				'faul_info', 'lefte_state' y 'right_state' lo son.
			Argumentos:
				state	-	Instancia de la clase State().
			Retorno:
				Una instancia de la clase State(), llamemosla 's', la cual 
				cumple que 's == state'.
		"""
		for x in self._states:
			if x == state:
				return x
		return None
	
	def get_init_state (self):
		"""
			Descripcion:
				Devuelve el estado inicial del sistema.
			Argumentos:
				No tiene.
			Retorno:
				Una instancia de la clase State() la cual es el estado inicial 
				del sistema.
		"""
		if self.init_state:
			return self.init_state
		else:
			raise LTSError("Initial state not established.")
	
	def get_state_set (self):
		"""
			Descripcion:
				Devuelve el conjunto de estados del sistema.
				NOTA: Devuelve una referencia al conjunto, no una copia.
			Argumentos:
				No tiene.
			Retorno:
				Una instancia de la clase Set() la cual es el conjunto de 
				estados del sistema.
		"""
		return self._states
	
	def get_state_count (self):
		"""
			Descripcion:
				Devuelve la cantodad de estados del sistema.
			Argumentos:
				No tiene.
			Retorno:
				Un entero que reprecenta la cantidad de esyados del sistema.
		"""
		return len(self._states)
	
	### Metodos para los eventos.
	
	def is_event (self, event, event_type):
		"""
			Descripcion:
				Dice si un evento pertenece o no al sistema.
			Argumentos:
				event		-	Cadena de caracteres que reprecenta un evento.
				event_type	-	Caracter que indica el tipo del evento.
			Retorno:
				True	-	Si 'event' es un evento del sistema.
				False	-	En caso contrario.
		"""
		return self._alphabet.is_event(event, event_type)
	
	def add_event (self, event, event_type):
		"""
			Descripcion:
				Agrega un evento al sistema.
			Argumentos:
				event		-	Cadena de caracteres que reprecenta un evento.
				event_type	-	Caracter que indica el tipo del evento.
			Retorno:
				No tiene.
		"""
		self._alphabet.add_event(event, event_type)
		self._recalc_tp = True
	
	def remove_event (self, event, event_type):
		"""
			Descripcion:
				Elimina un evento del sistema.
			Argumentos:
				event		-	Cadena de caracteres que reprecenta un evento.
				event_type	-	Caracter que indica el tipo del evento.
			Retorno:
				No tiene.
		"""
		self._alphabet.remove_event(event, event_type)
		self._recalc_tp = True
	
	def get_event_set (self, event_type):
		"""
			Descripcion:
				Devuelve el conjunto de eventos de determinado tipo del sistema.
				NOTA: Devuelve una referencia al conjunto, no una copia.
			Argumentos:
				event_type	-	Caracter que indica el tipo del evento.
			Retorno:
				Una instancia de la clase Set() la cual es el conjunto de 
				eventos de tipo 'event_type' del sistema.
		"""
		return self._alphabet.get_event_set(event_type)
	
	### Metodos para las transiciones.
	
	def add_transition (self, s_from, event, s_to):
		"""
			Descripcion:
				Agrega una transicion entre dos estados del sistema.
				NOTA: Los estados entre los cuales se agrega la transicion deben 
				existir en el sistema.
			Argumentos:
				s_from	-	Instancia de la clase State(). Este es el estado 
							desde donde sale la transicion, es decir, el estado
							de origen.
				event	-	Nombre del evento de la transicion a agregar.
				s_to	-	Instancia de la clase State(). Este es el estado 
							a donde termina la transicion, es decir, el estado
							de llegada.
			Retorno:
				No tiene.
		"""
		# Me fijo si existen los estados.
		if not self.is_state(s_from):
			raise LTSError("Source state not found", s_from.name)
		else:
			s_from = self.get_state(s_from)
		if not self.is_state(s_to):
			raise LTSError("Destination state not found", s_to.name)
		else:
			s_to = self.get_state(s_to)
		s_from.add_neighbor(event, s_to)
		self._recalc_tp = True
	
	def remove_transition (self, s_from, event,  s_to):
		"""
			Descripcion:
				Elimina una transicion entre dos estados.
			Argumentos:
				s_from	-	Instancia de la clase State(). Este es el estado 
							desde donde sale la transicion, es decir, el estado
							de origen.
				event	-	Nombre del evento de la transicion a eliminar.
				s_to	-	Instancia de la clase State(). Este es el estado 
							a donde termina la transicion, es decir, el estado
							de llegada.
			Retorno:
				No tiene.
		"""
		# Me fijo si existen los estados.
		if not self.is_state(s_from):
			raise LTSError("Source state not found", s_from.name)
		else:
			s_from = self.get_state(s_from)
		if not self.is_state(s_to):
			raise LTSError("Destination state not found", s_to.name)
		else:
			s_to = self.get_state(s_to)
		s_from.remove_neighbor(event, s_to)
		self._recalc_tp = True
	
	def get_transition_set (self):
		"""
			Descripcion:
				Devuelve el conjunto de transiciones del sistema.
			Argumentos:
				No tiene.
			Retorno:
				Un conjunto que contiene las transiciones del sistema. Los 
				elementos del conjunto son 3-uplas con el siguiente formato:
				(n,e,n') indicando que hay una transicion de la forma n -e-> n',
				donde n y n' son instancias de State() y 'e' es un evento.
				
		"""
		x = [(s,t[0],t[1]) for s in self._states for t in s.get_neighbor_set()]
		return set(x)
	
	def exist_transition (self, s_from, event, s_to):
		"""
			Descripcion:
				Dice si existe una transicion de la forma  "s_from -e-> s_to".
			Argumentos:
				s_from	-	Instancia de la clase State(). Este es el estado 
							desde donde sale la transicion, es decir, el estado
							de origen.
				event	-	Nombre del evento de la transicion a buscar.
				s_to	-	Instancia de la clase State(). Este es el estado 
							a donde termina la transicion, es decir, el estado
							de llegada.
			Retorno:
				True	-	Si la transicion "s_from -e-> s_to" existe en el 
							sistema.
				False	-	En caso contrario.
		"""
		x = (s_from, event, s_to)
		return x in [(s,t[0],t[1]) for s in self._states \
					for t in s.get_neighbor_set()]
	
	### Metodos de operacion.
	
	def get_diagnoser (self, label=''):
		"""
			Descripcion:
				Calcula y devuelve el 'diagnoser' del sistema.
			Argumentos:
				label	-	Opcional. Es una cadena de caracteres que permite 
							especificar el nombre del diagnoser.
			Retorno:
				Una instancia de la clase LTS() la cual reprecenta al 
				'diagnoser' del sistema.
		"""
		# Creo el Diagnoser.
		diagnoser = LTS()
		# Busco el estado inicial de 'self'.
		s0 = self.get_init_state()
		# Creo el estado inicial del diagnoser.
		d0 = State(s0.name, True)
		d0.fault_info = set()
		# Agrego el estado inicial del diagnoser.
		diagnoser.add_state(d0)
		# Quien Agrego a Quien! (Who Added Who)
		waw = dict()
		# Creo la cola para hacer BFS.
		queue = [(d0,d0,d0)]
		# Mientras no se vacie la cola...
		while queue:
			# Tomo el primer elemento de la cola.
			dstate,pre_dstate,bstate = queue.pop(0)
			# Agrego los vecinos no visitados de 'dstate'.
			state = self.get_states_by_name(dstate.name)[0]
			for e,s in state.get_neighbor_set():
				new_dstate = State(s.name, False)
				new_dstate.fault_info = set(dstate.fault_info)
				# Si el evento es una falla la agrego al conjunto de fallas.
				if self.is_event(e, 'f'):
					new_dstate.fault_info.add(e)
				# Me fijo si el estado ya existe en el diagnoser.
				if diagnoser.is_state(new_dstate): # Si ya existe, lo tomo. 
					new_dstate = diagnoser.get_state(new_dstate)
				else: # Si no existe lo agrego.
					diagnoser.add_state(new_dstate)
				# Si es observable tengo que agregar la transicion al diagonser.
				if self.is_event(e, 'o'):
					diagnoser.add_transition(pre_dstate, e, new_dstate)
					diagnoser.add_event(e, 'o')
					new_pre_dstate = new_dstate
				else:
					new_pre_dstate = pre_dstate
				if not waw.has_key(str(dstate)):
					waw[str(dstate)] = []
				if (new_dstate,bstate) in waw[str(dstate)]:
					continue
				else: # Si no, lo agrego a la cola.
					queue.append((new_dstate,new_pre_dstate,dstate))
					waw[str(dstate)].append((new_dstate,bstate))
			# Marco el estado como visitado.
			dstate.visited = True
		# Elimino los estados que no tienen transiciones salientes.
		self._remove_deadlock_states(diagnoser)
		# Le ponemos un nombre al diagnoser.
		if label: diagnoser.name = '('+label+')'+'-diagnoser-'+self.name
		else: diagnoser.name = 'diagnoser-'+self.name
		return diagnoser
	
	def get_twinplant (self):
		"""
			Descripcion:
				Construlle y devuelve la twnplant del sistema.
				NOTA: Por cuestiones de eficiencia llamadas sucesivas a esta 
				funcion no hacen que la twin-plant sea recalculada. La misma
				es recalculada solo si el sistema ha sido modificado.
			Argumentos:
				No tiene.
			Retorno:
				Una instancia de la clase LTS() que reprecenta la twin-plant del
				sistema.
		"""
		if self._recalc_tp:
			# Creo el diagnoser "izquierdo".
			left_diagnoser = self.get_diagnoser('L')
			# Creo el diagnoser "derecho".
			right_diagnoser = self.get_diagnoser('R')
			# Sincronizo en los eventos observables.
			sync_set = self.get_event_set('o')
			# Creo la twinplant sincronizando los Dagnoser.
			self._twinplant = left_diagnoser.sync(right_diagnoser, sync_set, None, True)
			# Le ponemos un nombre a la twinplant.
			self._twinplant.name = 'twinplant-'+self.name
			self._recalc_tp = False
		return self._twinplant
	
	def sync (self, g, sync_set=None, name=None, s_ref=False, rm_dstates=True):
		"""
			Descripcion:
				Calcula y devuelve la composicion en paralelo entre dos 
				sistemas.
				Por defecto se sincroniza en el conjunto de eventos de
				sincronizacion.
			Argumentos:
				g			-	Instancia de la clase LTS(). Es el sistema con 
								el cual se quiere componer a 'self'.
				sync_set	-	Opcional. Instancia de la clase SET() la cual 
								tiene el conjunto de eventos en los cuales se
								quiere sincronizar.
				name		-	Opcional. Cadena de caracteres que permite 
								especificar un nombre para el nuevo sistema.
				s_ref		-	Opcional. Es un booleano que dice si se eliminan
								o no las referencias de cada estado del nuevo 
								sistema a los estados de los sistemas 
								anteriores. Basicamente un estado en un sistema 
								compuesto esta formado por la union de dos 
								estados de los sistemas a componer, este 'flag' 
								permite decidir si la referencia a esos estados 
								se guarda o no. Por defecto estas referencias se
								elimianan, y solo son utilizadas cuando se 
								construye una twin-plant.
				rm_dstates	-	Opcional. Es un booleano que le dice al metodo 
								si tiene que eliminar los 'deadlock states' 
								luego de la composicion. Por defecto su valor es
								TRUE.
			Retorno:
				Una instancia de la clase LTS() la cual es la composicion en 
				paralelo de los sistemas 'self' y 'g'.
		"""
		sync_set = self._calculate_sync_set(g, sync_set)
		# Creo el LTS resultante.
		lts = LTS()
		# Creo el alfabateo.
		lts.set_alphabet(self.get_alphabet().union(g.get_alphabet()))
		# Cola para hacer BFS.
		queue = []
		# Creo el estado inicial.
		x = self.get_init_state()
		y = g.get_init_state()
		s = State(x.name+'-'+y.name, True)
		s.left_state = x
		s.right_state = y
		# Lo agrego al LTS.
		lts.add_state(s)
		# Lo pongo en la cola.
		queue.append(s)
		# Mientras no sea vacia la cola...
		while queue:
			# Tomo al prmer elemento de la cola.
			state = queue.pop(0)
			# Busco vecinos para ese elemento.
			self._sync_search_transition(state, queue, lts, sync_set)
		# Le ponemos un nombre al lts.
		if name: lts.name = name
		else: lts.name = (self.name.replace('.aut', ''))+'-'+g.name
		# Elimino la referencia a los estados.
		if not s_ref:
			for state in lts.get_state_set():
				state.left_state = None
				state.right_state = None
		# Elimino los estados que no tienen transiciones salientes.
		lts = self._remove_deadlock_states(lts)
		return lts
	
	def is_diagnosable (self, fault_set, verbose=False):
		"""
			Descripcion:
				Dice si el sistema es o no diagnosticable.
			Argumentos:
				fault_set	-	Conjunto de fallas para las cuales se quiere 
								saber si el sistema es diagnosticable o no.
				verbose		-	Opcional. Es un booleano que le indoca al metodo
								si debe mostrar informacion por la salida 
								estandar o no.
			Retorno:
				Devuelve una instancia de la clase Dict() que contiene 
				informacion sobre la diagnosticabilidad del sistema.
				Con la clave 'is_diag' se accede a un valor booleano que dice si
				el sistema es diagnosticable o no. Con la clave 'fault_list' se 
				accede a una lista la cual contiene informacion de las fallas no
				diagnosticables; los elementos de esta lista son tuplas con el 
				siguiente formato: (f,path) donde 'path' es el camino de la 
				twin-plant del sistema que atestigua que la falla 'f' no es 
				diagnosticable. Por ejemplo si el sistema es diagnosticable para
				todas las fallas el valor de retorno sera:
					{'is_diag':True,'fault_list':[]}
		"""
		result = dict()
		result['is_diag'] = True
		result['fault_list'] = [] 
		twinplant = self.get_twinplant()
		# to_file(twinplant) -> Este metodo no deberia generar este archivo.
		fault_set = self.get_event_set('f').intersection(fault_set)
		for f in fault_set:
			path = self._find_undecidible_path(twinplant, f)
			if not path == []:
				result['is_diag'] = False
				result['fault_list'].append((f,path))
				if verbose: print '   ',f,"is non-diagnosable."
			else:
				if verbose: print '   ',f,"is diagnosable."
		return result
	
	def list_paths (self):
		"""
			Descripcion:
				Lista todos los caminos del sistema que contienen un solo ciclo.
			Argumentos:
				No tiene.
			Retorno:
				Una lista que contine los caminos del sistema en los cuales hay 
				exactamente un ciclo. Los caminos son listas con el siguiente 
				formato: [s0,e0,s1,e1,...] donde los elementos "s_i" son 
				instancias de la clase State() y los elementos "e_i" son eventos
				(cadena de caracteres).
		"""
		# Lista donde voy a almacenar los caminos.
		path_list = []
		# Preparo la pila para hacer DFS. Los elementos de la pila seran de la forma
		# (S,E,L) donde S es un estado, E es el evento con el que se puso a S en la
		# pila, y L es la lista de vecinos visitado de S.
		stack = []
		# Tomo el estado incial del sistema
		s0 = self.get_init_state()
		# Pongo el primer elemento de la pila.
		stack.append((s0,'',[]))
		# Cuenta la cantidad de caminos.
		i = 0
		# Mientras no se vacie la pila.
		while stack:
			# Apunto al tope de la pila (no hago pop).
			state,event,visited_list = stack[_TOP_OF_THE_STACK]
			# Flag para saber si recorri todos los vecinos de 'state'.
			visit_all_neighbors = True
			# Recorro los vecinos de 'state'.
			for e,x in state.get_neighbor_set():
				# Si el estado ya fue visitado busco el siguiente.
				if (e,x) in visited_list: continue
				# Si no fue visitado me fijo si esta en la pila.
				if x in [t[0] for t in stack]:
					i += 1
					if i % 10000 == 0:
						os.write(1,str(i)+'\r')
					# Si esta en la pila ==> Encontre un ciclo.
					# Pongo a 'x' en la pila.
					stack.append((x,e,[]))
					# Convierto la pila en un camino y lo agrego a la lista.
					path_list.append(utils.stack_to_path(stack))
					# Saco a 'x' de la pila y sigo.
					stack.pop()
				else:
					# Si no fue visitado y no estaba en la pila lo pongo como
					# visitado, lo pongo en la pila y comienzo de nuevo el ciclo.
					visited_list.append((e,x))
					stack.append((x,e,[]))
					visit_all_neighbors = False
					break
			# Me fijo si sali porque visite a todos los vecinos de 'state' o porque
			# puse a alguien nuevo en la pila.
			if visit_all_neighbors:
				# Si visite a todos los vecinos saco a 'state' de la pila.
				stack.pop()
		# Total de caminos.
		print "Total de caminos:", str(i)
		return path_list
	
	def reduce_by_faults (self, fault_set):
		"""
			Descripcion:
				Reduce el sistema para el conjunto de fallas especificadas.
				Reducir el sistema significa eliminar las transiciones que 
				tienen como eventos a las fallas de 'fault_set' y luego tomar 
				la componente conexa que tiene al estado inicial como el nuevo 
				sistema.
				NOTA: Este metodo no modifica al objeto que lo llama, se crea 
				un nuevo sistema que es la reduccion del objeto llamador.
			Argumentos:
				fault_set	-	Conjunto de fallas para las cuales se quiere 
								reducir el sistema.
			Retorno:
				Devuelve una nueva instancia de la clase LTS() que es la 
				reduccion del sistema 'self' para las fallas especificadas en
				'fault_set'.
		"""
		# Tomo el conjunto de estados del sistema.
		states = self.get_state_set()
		# Lista de transiciones a eliminar.
		deleted_transitions = []
		# Para cada estado reviso sus transiciones salientes.
		for state in states:
			# Obtengo la relacion de vecino.
			neighbors = state.get_neighbor_set()
			for t in neighbors:
				if t[0] in fault_set:
					deleted_transitions.append(t)
		# Ahora tengo que armar el nuevo sistema.
		reduced_system = LTS()
		# Copio el alfabeto.
		reduced_system.set_alphabet(self.get_alphabet().__copy__())
		# Creo el estado inicial.
		init_state = State(self.get_init_state().name, True)
		reduced_system.add_state(init_state)
		# Cola para hacer BFS.
		queue = []
		# Pongo el estado inicial en la cola.
		queue.append(init_state)
		# Mientras no sea vacia la cola...
		while queue:
			# Tomo al primer elemento de la cola.
			state = queue.pop(0)
			if state.visited:
				continue
			# Lo marco como visitado.
			state.visited = True
			# Busco el estado correspondiente el 'self'.
			self_state = self.get_states_by_name(state.name)[0]
			# Agrego los vecinos de ese estado.
			neighbors = self_state.get_neighbor_set()
			for (e,s) in neighbors:
				if not (e,s) in deleted_transitions:
					new_state = reduced_system.get_states_by_name(s.name)
					if new_state == []:
						new_state = State(s.name, False)
						reduced_system.add_state(new_state)
					else:
						new_state = new_state[0]				
					reduced_system.add_transition(state,e,new_state)
					if not new_state.visited:
						queue.append(s)
		# Le ponemos un nombre a reduced_system.
		reduced_system.name = 'R'+(self.name.replace('.aut', ''))
		# Devolvemos el sitema reducido.
		return reduced_system

	def _find_undecidible_path (self, twinplant, fault):
		"""
			Descripcion:
				Busca un camino 'indeceable' para una falla determinada en la 
				twin-plant del sistema.
				Un camino indeceable es aquel en el que hay un clico de estados 
				indeceables con al menos un evento observable dentro del ciclo.
			Argumentos:
				twinplant	-	Una instancia de la clase LTS() que reprecenta 
								una twin-plant sobre la que se buscara un camino
								indeceable.
				fault		-	La falla para la que se busca un camino 
								indeceable.
			Retorno:
				Devuelve un camino. Un camino es una lista con el siguiente 
				formato: [s0,e0,s1,e1,...] donde los elementos "s_i" son 
				instancias de la clase State() y los elementos "e_i" son 
				eventos (cadena de caracteres).
		"""
		# Busco el estado inicial de la twinplant.
		s0 = twinplant.get_init_state()
		# Creo la pila para hacer DFS. Los elementos de la pila seran ternas de la
		# forma (s,e,l) donde: 's' es un estado, 'e' es el evento con el que se puso
		# a 's' en la pila, y 'l' es la lista de vecinos visitadoa de 's'.
		stack = [(s0,'',[])]
		# Flag para la terminacion del cliclo.
		find_path = False
		# Hago DFS para buscar el camino.
		while not find_path and stack:
			# Apunto al tope de la pila (no hago pop).
			state,event,visited_list = stack[_TOP_OF_THE_STACK]
			# Flag para saber si recorri todos los vecinos de 'state'.
			visit_all_neighbors = True
			# Recorro los vecinos de 'state'.
			for e,x in state.get_neighbor_set():
				# Si el estado ya fue visitado busco el siguiente.
				if x in visited_list: continue
				# Si no fue visitado me fijo si esta en la pila.
				if x in [t[0] for t in stack]:
					# Si esta en la pila ==> Encontre un ciclo.
					# Pongo a 'x' en la pila.
					stack.append((x,e,[]))
					# Me fijo si es un camino indecidible para 'fault'.
					if self._is_undecidible_path(stack,fault):
						# Encontre lo que buscaba !!!
						visit_all_neighbors = False
						find_path = True
						break
					else:
						# Si no, saco a 'x' de la pila y sigo.
						stack.pop()
						# Pongo a 'x' en la lista de visitados de 'state'.
						visited_list.append(x)
				else:
					# Si no fue visitado y no estaba en la pila lo pongo como
					# visitado y lo pongo en la pila.
					visited_list.append(x)
					stack.append((x,e,[]))
					visit_all_neighbors = False
					break
			# Me fijo si sali porque visite a todos los vecinos de 'state' o porque
			# puse a alguien nuevo en la pila.
			if visit_all_neighbors:
				# Si visite a todos los vecinos saco a 'state' de la pila.
				stack.pop()
		# Si encontre un camino indecidible armo la lista que voy a retornar.
		if find_path:
			return utils.stack_to_path(stack)
		else:
			return []

	def _is_undecidible_path (self, path, fault):
		"""
			Descripcion:
				Dice si un camino es indecidible para una determinada falla.
			Argumentos:
				path	-	Es una lista que reprecenta un camino y tiene el
							siguiente formato: [s0,e0,s1,e1,...] donde los 
							elementos "s_i" son instancias de la clase State() 
							y los elementos "e_i" son eventos (cadena de 
							caracteres).
				fault	-	Es la falla (cadena de caracteres) para el cual se
							quiere saber si el camino es indeceable o no.
			Retorno:
				True	-	Si 'path' es indeceable para 'fault'.
				False	-	En caso contrario.
		"""
		# Dice si todos los estados del ciclo son indecidibles o no.
		all_states_undecidible = True
		# Dice si hay o no al menos un evento observable dentro del ciclo.
		exist_observable_event = False
		# Tomo el ultimo estado del camino.
		last_state = (path[-1])[0]
		for i in range(1, len(path)+1):
			# Para recorrer 'path' de atras hacia adelente.
			i *= -1
			# Leo el estado y el evento.
			state,event,l = path[i]
			# Me fijo si el evento es observable.
			if event.startswith('o'):
				exist_observable_event = True
			# Me fijo si el estado es indecidible.
			if not self._is_undecidible_state(state, fault):
				all_states_undecidible = False
			# Si llego a un estado identico al ultimo estado, es porque recorri todo
			# el ciclo ==> Termino.
			if state == last_state:
				break
		if all_states_undecidible and exist_observable_event:
			return True
		else:
			return False

	def _is_undecidible_state (self, state, fault):
		"""
			Descripcion:
				Dice si un estado es indecidible para una determinada falla.
			Argumentos:
				state	-	Instancia de la clase State() la cual se quiere
							saber si es indeceable o no.
				fault	-	Es la falla (cadena de caracteres) para la cual se 
							quiere saber si el estado 'state' es indeceable.
			Retorno:
				True	-	Si 'state' es un estado indeceable para 'fault'.
				False	-	En caso contrario.
		"""
		left_fault_info = state.left_state.get_fault_info()
		right_fault_info = state.right_state.get_fault_info()
		s1 = left_fault_info.union(right_fault_info)
		s2 = left_fault_info.intersection(right_fault_info)
		if (fault in s1 and not fault in s2) or (not fault in s1 and fault in s2):
			return True
		else:
			return False
		
	def _remove_deadlock_states(self, lts):
		"""
			Descripcion:
				Elimina todos los estdos del sistema que esten "muertos", es 
				decir, aquellos estados que no sean alcanzables desde el estado 
				inicial o que no tengan transiciones salientes.
			Argumentos:
				lts		-	Instancia de la clase LTS() a la cual se le quieren 
							remover los estados "muertos".
			Retorno:
				Devuelve el sistema modificado.
		"""
		finished = False
		while not finished:
			states_to_remove = set([])
			for s1 in lts.get_state_set():
				# Si tiene transiciones salientes, o es el estado inicial, sigo 
				# con el sieguieinte estado.
				if s1.get_neighbor_set() or s1.init:
					continue
				# Si no, lo elimino de la lista de vecinos de los demas estados.
				for s2 in lts.get_state_set():
					# Si no tiene a s1 como vecino, sigo con el sieguiente.
					if not s2.is_neighbor(s1):
						continue
					# Si lo tiene como vecino, elimino todas las transiciones.
					nb = s2.get_neighbor_set()
					aux = set([t for t in nb if t[1]!=s1])
					s2.reset_neighbor_set()
					for e,n in aux:
						s2.add_neighbor(e,n)
				# Marco a s1 como un estado para eliminar.
				states_to_remove.add(s1)
			# Elimino los estados muertos.
			if states_to_remove:
				for s in states_to_remove:
					if not s.init:
						lts.remove_state(s)
			else:
				finished = True
		return lts
	
	def _calculate_sync_set (self, system, sync_set=None):
		"""
			Descripcion:
				Calcula el conjunto de sincronizacion entre dos sistemas.
				Si 'sync_set' es especificado entonces luego de calcular el 
				conjunto de sincronizacion este es restringido a los elementos 
				que hay en 'sync_set'.
			Argumentos:
				system		-	Instancia de la clase LTS().
				sync_set	-	Conjunto de eventos.
			Retorno:
				Devuelve el conjunto de sincronizacion entre 'self' y 'system',
				ademas si 'sync_set' es especificado el conjunto se restringe
				a los elementos de 'sync_set'.
		"""
		if sync_set == None:
			slef_events = self.get_event_set('o')
			system_events = system.get_event_set('o')
			sync_set = slef_events.intersection(system_events)
		else:
			o_self_events = self.get_event_set('o')
			o_system_events = system.get_event_set('o')
			o_sync_set = o_self_events.intersection(o_system_events)
			sync_set = sync_set.intersection(o_sync_set)
		return sync_set
	
	def _sync_search_transition (self, state, queue, lts, sync_set):
		"""
			Descripcion:
				Submetodo del metodo 'sync()'.
				Se encarga de agregar transiciones al nuevo sistema que se esta
				componiendo.
			Argumentos:
				state	 -	Instancia de la clase State().
				queue	 -	Lista que reprecenta una cola.
				lts		 -	Instancia de la clase LTS().
				sync_set -	Conjunto de eventos de sincronizacion.
			Retorno:
				No tiene.
		"""
		x = state.left_state
		y = state.right_state
		# Recorremos todos los vecinos de 'x'.
		for (e1,n1) in x.get_neighbor_set():
			if not e1 in sync_set:
				# Si el evento de la transicion no es de sincronizacion, me
				# puedo mover al otro estado sin problemas.
				# Busco el estado de llegada.
				s_to = State(n1.name+'-'+y.name, n1.init and y.init)
				s_to.left_state = n1
				s_to.right_state = y
				# Si no esta en el lts lo agregamos.
				if not lts.is_state(s_to): lts.add_state(s_to)
				else: s_to = lts.get_state(s_to)
				# Agrego la transicion.
				lts.add_transition(state, e1, s_to)
				lts.add_event(e1, e1[0])
				# Si no fue visitado lo encolamos.
				if not s_to.visited:
					s_to.visited = True
					queue.append(s_to)
			else:
				# Si el evento es de sincronizacion entonces debo ver si el 
				# estado 'y' tiene alguna transicion con ese evento.
				for (e2,n2) in y.get_neighbor_set():
					if e1 == e2:
						# Busco el estado de destino.
						n_to = n1.name+'-'+n2.name
						s_to = State(n_to, n1.init and n2.init)
						s_to.left_state = n1
						s_to.right_state = n2
						if not lts.is_state(s_to): lts.add_state(s_to)
						else: s_to = lts.get_state(s_to)
						lts.add_transition(state, e2, s_to)
						lts.add_event(e2, e2[0])
						# Si no fue visitado lo encolamos.
						if not s_to.visited:
							s_to.visited = True
							queue.append(s_to)
		# Recorremos todos los vecinos de 'y'.
		for (e1,n1) in y.get_neighbor_set():
			if not e1 in sync_set:
				# Si el evento de la transicion no es de sincronizacion, me
				# puedo mover al otro estado sin problemas.
				# Bsco el estado de destino.
				s_to = State(x.name+'-'+n1.name, x.init and n1.init)
				s_to.left_state = x
				s_to.right_state = n1
				if not lts.is_state(s_to): lts.add_state(s_to)
				else: s_to = lts.get_state(s_to)
				lts.add_transition(state, e1, s_to)
				lts.add_event(e1, e1[0])
				# Si no fue visitado lo encolamos.
				if not s_to.visited:
					s_to.visited = True
					queue.append(s_to)
			else:
				for (e2,n2) in x.get_neighbor_set():
					if e1 == e2:
						# Busco el estado de destino.
						n_to = n2.name+'-'+n1.name
						s_to = State(n_to, n2.init and n1.init)
						s_to.left_state = n2
						s_to.right_state = n1
						if not lts.is_state(s_to): lts.add_state(s_to)
						else: s_to = lts.get_state(s_to)
						lts.add_transition(state, e2, s_to)
						lts.add_event(e2, e2[0])
						# Si no fue visitado lo encolamos.
						if not s_to.visited:
							s_to.visited = True
							queue.append(s_to)
